Nuprl Lemma : first_wf
0,22
postcript
pdf
E
:Type,
pred?
:(
E
(
E
+Unit)),
e
:
E
. first(
e
)
latex
Definitions
first(
e
)
,
b
,
isl(
x
)
,
x
:
A
.
B
(
x
)
,
Unit
,
t
T
Lemmas
unit
wf
,
isl
wf
,
bnot
wf
origin
E:Type, pred?:(E
(E+Unit)), e:E. first(e) 
E:Type, pred?:(E(E+Unit)), e:E. first(e) 
bx:A. B(x) T